<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>StlcProp: Properties of STLC</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 2: Programming Language Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">StlcProp<span class="subtitle">Properties of STLC</span></h1>

<div class="code">
</div>

<div class="code">

<br/>
<span class="id" title="keyword">Set</span> <span class="id" title="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Maps</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Types.html#"><span class="id" title="library">Types</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Stlc.html#"><span class="id" title="library">Stlc</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Smallstep.html#"><span class="id" title="library">Smallstep</span></a>.<br/>
<span class="id" title="keyword">Module</span> <a id="STLCProp" class="idref" href="#STLCProp"><span class="id" title="module">STLCProp</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">STLC</span>.<br/>
</div>

<div class="doc">
In this chapter, we develop the fundamental theory of the Simply
    Typed Lambda Calculus -- in particular, the type safety
    theorem. 
</div>

<div class="doc">
<a id="lab234"></a><h1 class="section">Canonical Forms</h1>

<div class="paragraph"> </div>

 As we saw for the very simple language in the <a href="Types.html"><span class="inlineref">Types</span></a>
    chapter, the first step in establishing basic properties of
    reduction and types is to identify the possible <i>canonical
    forms</i> (i.e., well-typed closed values) belonging to each type.
    For <span class="inlinecode"><span class="id" title="var">Bool</span></span>, these are again the boolean values <span class="inlinecode"><span class="id" title="var">true</span></span> and <span class="inlinecode"><span class="id" title="var">false</span></span>;
    for arrow types, they are lambda-abstractions.  
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCProp.canonical_forms_bool" class="idref" href="#STLCProp.canonical_forms_bool"><span class="id" title="lemma">canonical_forms_bool</span></a> : <span class="id" title="keyword">∀</span> <a id="t:1" class="idref" href="#t:1"><span class="id" title="binder">t</span></a>,<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:1"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#STLC.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="StlcProp.html#t:1"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="StlcProp.html#t:1"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="StlcProp.html#t:1"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">)</span></a>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">HT</span> <span class="id" title="var">HVal</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">HVal</span>; <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">HT</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCProp.canonical_forms_fun" class="idref" href="#STLCProp.canonical_forms_fun"><span class="id" title="lemma">canonical_forms_fun</span></a> : <span class="id" title="keyword">∀</span> <a id="t:2" class="idref" href="#t:2"><span class="id" title="binder">t</span></a> <a id="T<sub>1</sub>:3" class="idref" href="#T<sub>1</sub>:3"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:4" class="idref" href="#T<sub>2</sub>:4"><span class="id" title="binder">T<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:2"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="StlcProp.html#T<sub>1</sub>:3"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#T<sub>2</sub>:4"><span class="id" title="variable">T<sub>2</sub></span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#STLC.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="StlcProp.html#t:2"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="x:5" class="idref" href="#x:5"><span class="id" title="binder">x</span></a> <a id="u:6" class="idref" href="#u:6"><span class="id" title="binder">u</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="StlcProp.html#t:2"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="StlcProp.html#x:5"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="StlcProp.html#T<sub>1</sub>:3"><span class="id" title="variable">T<sub>1</sub></span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="StlcProp.html#u:6"><span class="id" title="variable">u</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="var">HT</span> <span class="id" title="var">HVal</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">HVal</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">HT</span>; <span class="id" title="tactic">subst</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">∃</span> <span class="id" title="var">x<sub>0</sub></span>, <span class="id" title="var">t<sub>1</sub></span>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab235"></a><h1 class="section">Progress</h1>

<div class="paragraph"> </div>

 The <i>progress</i> theorem tells us that closed, well-typed
    terms are not stuck: either a well-typed term is a value, or it
    can take a reduction step.  The proof is a relatively
    straightforward extension of the progress proof we saw in the
    <a href="Types.html"><span class="inlineref">Types</span></a> chapter.  We give the proof in English first, then
    the formal version. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="STLCProp.progress" class="idref" href="#STLCProp.progress"><span class="id" title="lemma">progress</span></a> : <span class="id" title="keyword">∀</span> <a id="t:7" class="idref" href="#t:7"><span class="id" title="binder">t</span></a> <a id="T:8" class="idref" href="#T:8"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:7"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:8"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#STLC.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="StlcProp.html#t:7"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="t':9" class="idref" href="#t':9"><span class="id" title="binder">t'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="StlcProp.html#t:7"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="StlcProp.html#t':9"><span class="id" title="variable">t'</span></a>.<br/>
</div>

<div class="doc">
<i>Proof</i>: By induction on the derivation of <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> The last rule of the derivation cannot be <span class="inlinecode"><span class="id" title="var">T_Var</span></span>, since a
      variable is never well typed in an empty context.

<div class="paragraph"> </div>


</li>
<li> The <span class="inlinecode"><span class="id" title="var">T_True</span></span>, <span class="inlinecode"><span class="id" title="var">T_False</span></span>, and <span class="inlinecode"><span class="id" title="var">T_Abs</span></span> cases are trivial, since in
      each of these cases we can see by inspecting the rule that <span class="inlinecode"><span class="id" title="var">t</span></span>
      is a value.

<div class="paragraph"> </div>


</li>
<li> If the last rule of the derivation is <span class="inlinecode"><span class="id" title="var">T_App</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> has the
      form <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> for some <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>, where <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">T</span></span>
      and <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span> for some type <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span>.  The induction hypothesis
      for the first subderivation says that either <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> is a value or
      else it can take a reduction step.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> is a value, then consider <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>, which by the
          induction hypothesis for the second subderivation must also
          either be a value or take a step.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> is a value.  Since <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> is a value with an
              arrow type, it must be a lambda abstraction; hence <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>
              <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> can take a step by <span class="inlinecode"><span class="id" title="var">ST_AppAbs</span></span>.

<div class="paragraph"> </div>


</li>
<li> Otherwise, <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> can take a step, and hence so can <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>
              <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> by <span class="inlinecode"><span class="id" title="var">ST_App2</span></span>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> can take a step, then so can <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> by <span class="inlinecode"><span class="id" title="var">ST_App1</span></span>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If the last rule of the derivation is <span class="inlinecode"><span class="id" title="var">T_If</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="keyword">if</span></span>
      <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>, where <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> has type <span class="inlinecode"><span class="id" title="var">Bool</span></span>.  The first IH
      says that <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> either is a value or takes a step.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> is a value, then since it has type <span class="inlinecode"><span class="id" title="var">Bool</span></span> it must be
          either <span class="inlinecode"><span class="id" title="var">true</span></span> or <span class="inlinecode"><span class="id" title="var">false</span></span>.  If it is <span class="inlinecode"><span class="id" title="var">true</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> steps to
          <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>; otherwise it steps to <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>.

<div class="paragraph"> </div>


</li>
<li> Otherwise, <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> takes a step, and therefore so does <span class="inlinecode"><span class="id" title="var">t</span></span> (by
          <span class="inlinecode"><span class="id" title="var">ST_If</span></span>). 
</li>
</ul>

</li>
</ul>

</div>
<div class="code">
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">Ht</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">remember</span> <span class="id" title="definition">empty</span> <span class="id" title="keyword">as</span> <span class="id" title="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Ht</span>; <span class="id" title="tactic">subst</span> <span class="id" title="var">Gamma</span>; <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;auto&nbsp;solves&nbsp;all&nbsp;three&nbsp;cases&nbsp;in&nbsp;which&nbsp;t&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;contradictory:&nbsp;variables&nbsp;cannot&nbsp;be&nbsp;typed&nbsp;in&nbsp;an<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;empty&nbsp;context&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">discriminate</span> <span class="id" title="var">H</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span>&nbsp;=&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>.&nbsp;&nbsp;Proceed&nbsp;by&nbsp;cases&nbsp;on&nbsp;whether&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>&nbsp;is&nbsp;a<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;value&nbsp;or&nbsp;steps...&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">right</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHt1</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHt2</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;× <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;is&nbsp;also&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="StlcProp.html#STLCProp.canonical_forms_fun"><span class="id" title="lemma">canonical_forms_fun</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">Ht<sub>1</sub></span>; [|<span class="id" title="tactic">assumption</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">Ht<sub>1</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">x</span> [<span class="id" title="var">t<sub>0</sub></span> <span class="id" title="var">H<sub>1</sub></span>]]. <span class="id" title="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">∃</span> (<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><span class="id" title="var">x</span><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a><span class="id" title="var">t<sub>0</sub></span> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;× <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">H<sub>0</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">t<sub>2</sub>'</span> <span class="id" title="var">Hstp</span>]. <span class="id" title="tactic">∃</span> (<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub>'</span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>)...<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">t<sub>1</sub>'</span> <span class="id" title="var">Hstp</span>]. <span class="id" title="tactic">∃</span> (<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">t<sub>1</sub>'</span> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>)...<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_If&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">right</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHt1</span>...<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<a class="idref" href="StlcProp.html#STLCProp.canonical_forms_bool"><span class="id" title="lemma">canonical_forms_bool</span></a> <span class="id" title="var">t<sub>1</sub></span>); <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">eauto</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;also&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">t<sub>1</sub>'</span> <span class="id" title="var">Hstp</span>]. <span class="id" title="tactic">∃</span> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <span class="id" title="var">t<sub>1</sub>'</span> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <span class="id" title="var">t<sub>3</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>...<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab236"></a><h4 class="section">Exercise: 3 stars, advanced (progress_from_term_ind)</h4>
 Show that progress can also be proved by induction on terms
    instead of induction on typing derivations. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="STLCProp.progress'" class="idref" href="#STLCProp.progress'"><span class="id" title="lemma">progress'</span></a> : <span class="id" title="keyword">∀</span> <a id="t:10" class="idref" href="#t:10"><span class="id" title="binder">t</span></a> <a id="T:11" class="idref" href="#T:11"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:10"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:11"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#STLC.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="StlcProp.html#t:10"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="t':12" class="idref" href="#t':12"><span class="id" title="binder">t'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="StlcProp.html#t:10"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="StlcProp.html#t':12"><span class="id" title="variable">t'</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">t</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">T</span> <span class="id" title="var">Ht</span>; <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab237"></a><h1 class="section">Preservation</h1>

<div class="paragraph"> </div>

 The other half of the type soundness property is the
    preservation of types during reduction.  For this part, we'll need
    to develop some technical machinery for reasoning about variables
    and substitution.  Working from top to bottom (from the high-level
    property we are actually interested in to the lowest-level
    technical lemmas that are needed by various cases of the more
    interesting proofs), the story goes like this:

<div class="paragraph"> </div>

<ul class="doclist">
<li> The <i>preservation theorem</i> is proved by induction on a typing
        derivation, pretty much as we did in the <a href="Types.html"><span class="inlineref">Types</span></a> chapter.
        The one case that is significantly different is the one for
        the <span class="inlinecode"><span class="id" title="var">ST_AppAbs</span></span> rule, whose definition uses the substitution
        operation.  To see that this step preserves typing, we need to
        know that the substitution itself does.  So we prove a...

<div class="paragraph"> </div>


</li>
<li> <i>substitution lemma</i>, stating that substituting a (closed)
        term <span class="inlinecode"><span class="id" title="var">s</span></span> for a variable <span class="inlinecode"><span class="id" title="var">x</span></span> in a term <span class="inlinecode"><span class="id" title="var">t</span></span> preserves the type
        of <span class="inlinecode"><span class="id" title="var">t</span></span>.  The proof goes by induction on the form of <span class="inlinecode"><span class="id" title="var">t</span></span> and
        requires looking at all the different cases in the definition
        of substitition.  This time, for the variables case, we
        discover that we need to deduce from the fact that a term
        <span class="inlinecode"><span class="id" title="var">s</span></span> has type S in the empty context the fact that <span class="inlinecode"><span class="id" title="var">s</span></span> has
        type S in every context. For this we prove a...

<div class="paragraph"> </div>


</li>
<li> <i>weakening</i> lemma, showing that typing is preserved under
        "extensions" to the context <span class="inlinecode"><span class="id" title="var">Gamma</span></span>.

</li>
</ul>

<div class="paragraph"> </div>

   To make Coq happy, of course, we need to formalize the story in the
   opposite order... 
</div>

<div class="doc">
<a id="lab238"></a><h2 class="section">The Weakening Lemma</h2>

<div class="paragraph"> </div>

 Typing is preserved under "extensions" to the context <span class="inlinecode"><span class="id" title="var">Gamma</span></span>.
    (Recall the definition of "inclusion" from Maps.v.) 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCProp.weakening" class="idref" href="#STLCProp.weakening"><span class="id" title="lemma">weakening</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:13" class="idref" href="#Gamma:13"><span class="id" title="binder">Gamma</span></a> <a id="Gamma':14" class="idref" href="#Gamma':14"><span class="id" title="binder">Gamma'</span></a> <a id="t:15" class="idref" href="#t:15"><span class="id" title="binder">t</span></a> <a id="T:16" class="idref" href="#T:16"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">inclusion</span> <a class="idref" href="StlcProp.html#Gamma:13"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="StlcProp.html#Gamma':14"><span class="id" title="variable">Gamma'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma:13"><span class="id" title="variable">Gamma</span></a>  <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:15"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:16"><span class="id" title="variable">T</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma':14"><span class="id" title="variable">Gamma'</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:15"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:16"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">Gamma'</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">H</span> <span class="id" title="var">Ht</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma'</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Ht</span>; <span class="id" title="tactic">eauto</span> <span class="id" title="keyword">using</span> <span class="id" title="lemma">inclusion_update</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The following simple corollary is useful below. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCProp.weakening_empty" class="idref" href="#STLCProp.weakening_empty"><span class="id" title="lemma">weakening_empty</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:17" class="idref" href="#Gamma:17"><span class="id" title="binder">Gamma</span></a> <a id="t:18" class="idref" href="#t:18"><span class="id" title="binder">t</span></a> <a id="T:19" class="idref" href="#T:19"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:18"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:19"><span class="id" title="variable">T</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma:17"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:18"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:19"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="StlcProp.html#STLCProp.weakening"><span class="id" title="lemma">weakening</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">discriminate</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab239"></a><h2 class="section">A Substitution Lemma</h2>

<div class="paragraph"> </div>

 Now we come to the conceptual heart of the proof that reduction
    preserves types -- namely, the observation that <i>substitution</i>
    preserves types. 
<div class="paragraph"> </div>

 Formally, the so-called <i>substitution lemma</i> says this:
    Suppose we have a term <span class="inlinecode"><span class="id" title="var">t</span></span> with a free variable <span class="inlinecode"><span class="id" title="var">x</span></span>, and suppose
    we've assigned a type <span class="inlinecode"><span class="id" title="var">T</span></span> to <span class="inlinecode"><span class="id" title="var">t</span></span> under the assumption that <span class="inlinecode"><span class="id" title="var">x</span></span> has
    some type <span class="inlinecode"><span class="id" title="var">U</span></span>.  Also, suppose that we have some other term <span class="inlinecode"><span class="id" title="var">v</span></span> and
    that we've shown that <span class="inlinecode"><span class="id" title="var">v</span></span> has type <span class="inlinecode"><span class="id" title="var">U</span></span>.  Then, since <span class="inlinecode"><span class="id" title="var">v</span></span> satisfies
    the assumption we made about <span class="inlinecode"><span class="id" title="var">x</span></span> when typing <span class="inlinecode"><span class="id" title="var">t</span></span>, we can
    substitute <span class="inlinecode"><span class="id" title="var">v</span></span> for each of the occurrences of <span class="inlinecode"><span class="id" title="var">x</span></span> in <span class="inlinecode"><span class="id" title="var">t</span></span> and
    obtain a new term that still has type <span class="inlinecode"><span class="id" title="var">T</span></span>. 
<div class="paragraph"> </div>

 <i>Lemma</i>: If <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> and <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">v</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">U</span></span>,
    then <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">v</span>]<span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCProp.substitution_preserves_typing" class="idref" href="#STLCProp.substitution_preserves_typing"><span class="id" title="lemma">substitution_preserves_typing</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:20" class="idref" href="#Gamma:20"><span class="id" title="binder">Gamma</span></a> <a id="x:21" class="idref" href="#x:21"><span class="id" title="binder">x</span></a> <a id="U:22" class="idref" href="#U:22"><span class="id" title="binder">U</span></a> <a id="t:23" class="idref" href="#t:23"><span class="id" title="binder">t</span></a> <a id="v:24" class="idref" href="#v:24"><span class="id" title="binder">v</span></a> <a id="T:25" class="idref" href="#T:25"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="StlcProp.html#x:21"><span class="id" title="variable">x</span></a> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="StlcProp.html#U:22"><span class="id" title="variable">U</span></a> <span class="id" title="notation">;</span> <a class="idref" href="StlcProp.html#Gamma:20"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:23"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:25"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#v:24"><span class="id" title="variable">v</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#U:22"><span class="id" title="variable">U</span></a>   <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma:20"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="StlcProp.html#x:21"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="StlcProp.html#v:24"><span class="id" title="variable">v</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a><a class="idref" href="StlcProp.html#t:23"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:25"><span class="id" title="variable">T</span></a>.<br/>
</div>

<div class="doc">
The substitution lemma can be viewed as a kind of "commutation
    property."  Intuitively, it says that substitution and typing can
    be done in either order: we can either assign types to the terms
    <span class="inlinecode"><span class="id" title="var">t</span></span> and <span class="inlinecode"><span class="id" title="var">v</span></span> separately (under suitable contexts) and then combine
    them using substitution, or we can substitute first and then
    assign a type to <span class="inlinecode"></span> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">v</span>]</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"></span>; the result is the same either
    way.

<div class="paragraph"> </div>

    <i>Proof</i>: We show, by induction on <span class="inlinecode"><span class="id" title="var">t</span></span>, that for all <span class="inlinecode"><span class="id" title="var">T</span></span> and
    <span class="inlinecode"><span class="id" title="var">Gamma</span></span>, if <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> and <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">v</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">U</span></span>, then
    <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">v</span>]<span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" title="var">t</span></span> is a variable there are two cases to consider,
        depending on whether <span class="inlinecode"><span class="id" title="var">t</span></span> is <span class="inlinecode"><span class="id" title="var">x</span></span> or some other variable.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">x</span></span>, then from the fact that <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span>
            <span class="inlinecode"><span class="id" title="var">T</span></span> we conclude that <span class="inlinecode"><span class="id" title="var">U</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">T</span></span>.  We must show that <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">v</span>]<span class="id" title="var">x</span></span> <span class="inlinecode">=</span>
            <span class="inlinecode"><span class="id" title="var">v</span></span> has type <span class="inlinecode"><span class="id" title="var">T</span></span> under <span class="inlinecode"><span class="id" title="var">Gamma</span></span>, given the assumption that
            <span class="inlinecode"><span class="id" title="var">v</span></span> has type <span class="inlinecode"><span class="id" title="var">U</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">T</span></span> under the empty context.  This
            follows from the weakening lemma.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" title="var">t</span></span> is some variable <span class="inlinecode"><span class="id" title="var">y</span></span> that is not equal to <span class="inlinecode"><span class="id" title="var">x</span></span>, then
            we need only note that <span class="inlinecode"><span class="id" title="var">y</span></span> has the same type under <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span>
            <span class="inlinecode"><span class="id" title="var">Gamma</span></span> as under <span class="inlinecode"><span class="id" title="var">Gamma</span></span>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If <span class="inlinecode"><span class="id" title="var">t</span></span> is an abstraction <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">S</span>,</span> <span class="inlinecode"><span class="id" title="var">t<sub>0</sub></span></span>, then <span class="inlinecode"><span class="id" title="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span>→<span class="id" title="var">T<sub>1</sub></span></span> and
        the IH tells us, for all <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> and <span class="inlinecode"><span class="id" title="var">T<sub>0</sub></span></span>, that if <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span>
        <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>0</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>0</sub></span></span>, then <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">v</span>]<span class="id" title="var">t<sub>0</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>0</sub></span></span>.
        Moreover, by inspecting the typing rules we see it must be
        the case that <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">S</span>;</span> <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>0</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>.

<div class="paragraph"> </div>

        The substitution in the conclusion behaves differently
        depending on whether <span class="inlinecode"><span class="id" title="var">x</span></span> and <span class="inlinecode"><span class="id" title="var">y</span></span> are the same variable.

<div class="paragraph"> </div>

        First, suppose <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">y</span></span>.  Then, by the definition of
        substitution, <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">v</span>]<span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">t</span></span>, so we just need to show <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span>
        <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.  Using <span class="inlinecode"><span class="id" title="var">T_Abs</span></span>, we need to show that <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">S</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span>
        <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>0</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>. But we know <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">S</span>;</span> <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>0</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>,
        and the claim follows since <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">y</span></span>.

<div class="paragraph"> </div>

        Second, suppose <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" title="var">y</span></span>. Again, using <span class="inlinecode"><span class="id" title="var">T_Abs</span></span>,
        we need to show that <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">S</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">v</span>]<span class="id" title="var">t<sub>0</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>.
        Since <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" title="var">y</span></span>, we have
        <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">S</span>;</span> <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span> <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">S</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span>. So,
        we have <span class="inlinecode"><span class="id" title="var">x</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">U</span>;</span> <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">S</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>0</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>. Then, the
        the IH applies (taking <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">S</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span>), giving us
        <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">S</span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">v</span>]<span class="id" title="var">t<sub>0</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>, as required.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" title="var">t</span></span> is an application <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>, the result follows
        straightforwardly from the definition of substitution and the
        induction hypotheses.

<div class="paragraph"> </div>


</li>
<li> The remaining cases are similar to the application case. 
</li>
</ul>

</div>
<div class="code">

<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">x</span> <span class="id" title="var">U</span> <span class="id" title="var">t</span> <span class="id" title="var">v</span> <span class="id" title="var">T</span> <span class="id" title="var">Ht</span> <span class="id" title="var">Hv</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma</span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">t</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">T</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">H</span>;<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;in&nbsp;each&nbsp;case,&nbsp;we'll&nbsp;want&nbsp;to&nbsp;get&nbsp;at&nbsp;the&nbsp;derivation&nbsp;of&nbsp;H&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">s</span> <span class="id" title="var">into</span> <span class="id" title="var">y</span>. <span class="id" title="tactic">destruct</span> (<span class="id" title="axiom">eqb_stringP</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>); <span class="id" title="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x=y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="lemma">update_eq</span> <span class="id" title="tactic">in</span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">injection</span> <span class="id" title="var">H<sub>2</sub></span> <span class="id" title="keyword">as</span> <span class="id" title="var">H<sub>2</sub></span>; <span class="id" title="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="StlcProp.html#STLCProp.weakening_empty"><span class="id" title="lemma">weakening_empty</span></a>. <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x&lt;&gt;y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.T_Var"><span class="id" title="constructor">T_Var</span></a>. <span class="id" title="tactic">rewrite</span> <span class="id" title="lemma">update_neq</span> <span class="id" title="tactic">in</span> <span class="id" title="var">H<sub>2</sub></span>; <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">s</span> <span class="id" title="var">into</span> <span class="id" title="var">y</span>, <span class="id" title="var">t</span> <span class="id" title="var">into</span> <span class="id" title="var">S</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<span class="id" title="axiom">eqb_stringP</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>); <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.T_Abs"><span class="id" title="constructor">T_Abs</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x=y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="lemma">update_shadow</span> <span class="id" title="tactic">in</span> <span class="id" title="var">H<sub>5</sub></span>. <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x&lt;&gt;y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">IHt</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="lemma">update_permute</span>; <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
One technical subtlety in the statement of the above lemma is that
    we assume <span class="inlinecode"><span class="id" title="var">v</span></span> has type <span class="inlinecode"><span class="id" title="var">U</span></span> in the <i>empty</i> context -- in other
    words, we assume <span class="inlinecode"><span class="id" title="var">v</span></span> is closed.  (Since we are using a simple
    definition of substition that is not capture-avoiding, it doesn't
    make sense to substitute non-closed terms into other terms.
    Fortunately, closed terms are all we need!)
 
<div class="paragraph"> </div>

<a id="lab240"></a><h4 class="section">Exercise: 3 stars, advanced (substitution_preserves_typing_from_typing_ind)</h4>
 Show that substitution_preserves_typing can also be
    proved by induction on typing derivations instead
    of induction on terms. 
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="STLCProp.substitution_preserves_typing_from_typing_ind" class="idref" href="#STLCProp.substitution_preserves_typing_from_typing_ind"><span class="id" title="lemma">substitution_preserves_typing_from_typing_ind</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:26" class="idref" href="#Gamma:26"><span class="id" title="binder">Gamma</span></a> <a id="x:27" class="idref" href="#x:27"><span class="id" title="binder">x</span></a> <a id="U:28" class="idref" href="#U:28"><span class="id" title="binder">U</span></a> <a id="t:29" class="idref" href="#t:29"><span class="id" title="binder">t</span></a> <a id="v:30" class="idref" href="#v:30"><span class="id" title="binder">v</span></a> <a id="T:31" class="idref" href="#T:31"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="StlcProp.html#x:27"><span class="id" title="variable">x</span></a> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="StlcProp.html#U:28"><span class="id" title="variable">U</span></a> <span class="id" title="notation">;</span> <a class="idref" href="StlcProp.html#Gamma:26"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:29"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:31"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#v:30"><span class="id" title="variable">v</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#U:28"><span class="id" title="variable">U</span></a>   <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma:26"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="StlcProp.html#x:27"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="StlcProp.html#v:30"><span class="id" title="variable">v</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a><a class="idref" href="StlcProp.html#t:29"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:31"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">x</span> <span class="id" title="var">U</span> <span class="id" title="var">t</span> <span class="id" title="var">v</span> <span class="id" title="var">T</span> <span class="id" title="var">Ht</span> <span class="id" title="var">Hv</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">remember</span> (<span class="id" title="var">x</span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="id" title="var">U</span><span class="id" title="notation">;</span> <span class="id" title="var">Gamma</span>) <span class="id" title="keyword">as</span> <span class="id" title="var">Gamma'</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Ht</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma'</span> <span class="id" title="var">G</span>; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab241"></a><h2 class="section">Main Theorem</h2>

<div class="paragraph"> </div>

 We now have the ingredients we need to prove preservation: if a
    closed term <span class="inlinecode"><span class="id" title="var">t</span></span> has type <span class="inlinecode"><span class="id" title="var">T</span></span> and takes a step to <span class="inlinecode"><span class="id" title="var">t'</span></span>, then <span class="inlinecode"><span class="id" title="var">t'</span></span>
    is also a closed term with type <span class="inlinecode"><span class="id" title="var">T</span></span>.  In other words, the
    small-step reduction relation preserves types. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="STLCProp.preservation" class="idref" href="#STLCProp.preservation"><span class="id" title="lemma">preservation</span></a> : <span class="id" title="keyword">∀</span> <a id="t:32" class="idref" href="#t:32"><span class="id" title="binder">t</span></a> <a id="t':33" class="idref" href="#t':33"><span class="id" title="binder">t'</span></a> <a id="T:34" class="idref" href="#T:34"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:32"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:34"><span class="id" title="variable">T</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="StlcProp.html#t:32"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="StlcProp.html#t':33"><span class="id" title="variable">t'</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t':33"><span class="id" title="variable">t'</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:34"><span class="id" title="variable">T</span></a>.<br/>
</div>

<div class="doc">
<i>Proof</i>: By induction on the derivation of <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> We can immediately rule out <span class="inlinecode"><span class="id" title="var">T_Var</span></span>, <span class="inlinecode"><span class="id" title="var">T_Abs</span></span>, <span class="inlinecode"><span class="id" title="var">T_True</span></span>, and
      <span class="inlinecode"><span class="id" title="var">T_False</span></span> as final rules in the derivation, since in each of these
      cases <span class="inlinecode"><span class="id" title="var">t</span></span> cannot take a step.

<div class="paragraph"> </div>


</li>
<li> If the last rule in the derivation is <span class="inlinecode"><span class="id" title="var">T_App</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>,
      and there are subderivations showing that <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span>→<span class="id" title="var">T</span></span> and
      <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span> plus two induction hypotheses: (1) <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span>
      implies <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span>→<span class="id" title="var">T</span></span> and (2) <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub>'</span></span> implies <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub>'</span></span>
      <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span>.  There are now three subcases to consider, one for
      each rule that could be used to show that <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> takes a step
      to <span class="inlinecode"><span class="id" title="var">t'</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> takes a step by <span class="inlinecode"><span class="id" title="var">ST_App1</span></span>, with <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> stepping to
          <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span>, then, by the first IH, <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> has the same type as
          <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> (<span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span>→<span class="id" title="var">T</span></span>), and hence by <span class="inlinecode"><span class="id" title="var">T_App</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> has
          type <span class="inlinecode"><span class="id" title="var">T</span></span>.

<div class="paragraph"> </div>


</li>
<li> The <span class="inlinecode"><span class="id" title="var">ST_App2</span></span> case is similar, using the second IH.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> takes a step by <span class="inlinecode"><span class="id" title="var">ST_AppAbs</span></span>, then <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span>
          <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">T<sub>0</sub></span>,<span class="id" title="var">t<sub>0</sub></span></span> and <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> steps to <span class="inlinecode">[<span class="id" title="var">x<sub>0</sub></span>:=<span class="id" title="var">t<sub>2</sub></span>]<span class="id" title="var">t<sub>0</sub></span></span>; the desired
          result now follows from the substitution lemma.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> If the last rule in the derivation is <span class="inlinecode"><span class="id" title="var">T_If</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="keyword">if</span></span>
      <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>, with <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">Bool</span></span>, <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>, and
      <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>, and with three induction hypotheses: (1) <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span>
      <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> implies <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">Bool</span></span>, (2) <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub>'</span></span> implies <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub>'</span></span>
      <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>, and (3) <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub>'</span></span> implies <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub>'</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>.

<div class="paragraph"> </div>

      There are again three subcases to consider, depending on how <span class="inlinecode"><span class="id" title="var">t</span></span>
      steps.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" title="var">t</span></span> steps to <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> or <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span> by <span class="inlinecode"><span class="id" title="var">ST_IfTrue</span></span> or
          <span class="inlinecode"><span class="id" title="var">ST_IfFalse</span></span>, the result is immediate, since <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>
          have the same type as <span class="inlinecode"><span class="id" title="var">t</span></span>.

<div class="paragraph"> </div>


</li>
<li> Otherwise, <span class="inlinecode"><span class="id" title="var">t</span></span> steps by <span class="inlinecode"><span class="id" title="var">ST_If</span></span>, and the desired
          conclusion follows directly from the first induction
          hypothesis. 
</li>
</ul>

</li>
</ul>

</div>
<div class="code">

<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">t'</span> <span class="id" title="var">T</span> <span class="id" title="var">HT</span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">t'</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">remember</span> <span class="id" title="definition">empty</span> <span class="id" title="keyword">as</span> <span class="id" title="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">HT</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t'</span> <span class="id" title="var">HE</span>; <span class="id" title="tactic">subst</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> <span class="id" title="tactic">solve</span> [<span class="id" title="tactic">inversion</span> <span class="id" title="var">HE</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">auto</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">HE</span>; <span class="id" title="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Most&nbsp;of&nbsp;the&nbsp;cases&nbsp;are&nbsp;immediate&nbsp;by&nbsp;induction,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="tactic">eauto</span></span>&nbsp;takes&nbsp;care&nbsp;of&nbsp;them&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_AppAbs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="StlcProp.html#STLCProp.substitution_preserves_typing"><span class="id" title="lemma">substitution_preserves_typing</span></a> <span class="id" title="keyword">with</span> <span class="id" title="var">T<sub>2</sub></span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">HT<sub>1</sub></span>...<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab242"></a><h4 class="section">Exercise: 2 stars, standard, especially useful (subject_expansion_stlc)</h4>
 An exercise in the <a href="Types.html"><span class="inlineref">Types</span></a> chapter asked about the <i>subject
    expansion</i> property for the simple language of arithmetic and
    boolean expressions.  This property did not hold for that language,
    and it also fails for STLC.  That is, it is not always the case that,
    if <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span> and <span class="inlinecode"><span class="id" title="var">has_type</span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>, then <span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.
    Show this by giving a counter-example that does <i>not involve
    conditionals</i>.

<div class="paragraph"> </div>

    You can state your counterexample informally in words, with a brief
    explanation. 
</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="STLCProp.manual_grade_for_subject_expansion_stlc" class="idref" href="#STLCProp.manual_grade_for_subject_expansion_stlc"><span class="id" title="definition">manual_grade_for_subject_expansion_stlc</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab243"></a><h1 class="section">Type Soundness</h1>

<div class="paragraph"> </div>

<a id="lab244"></a><h4 class="section">Exercise: 2 stars, standard, optional (type_soundness)</h4>
 Put progress and preservation together and show that a well-typed
    term can <i>never</i> reach a stuck state.  
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="STLCProp.stuck" class="idref" href="#STLCProp.stuck"><span class="id" title="definition">stuck</span></a> (<a id="t:35" class="idref" href="#t:35"><span class="id" title="binder">t</span></a>:<a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a>) : <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;(<a class="idref" href="Smallstep.html#normal_form"><span class="id" title="definition">normal_form</span></a> <a class="idref" href="Stlc.html#STLC.step"><span class="id" title="inductive">step</span></a>) <a class="idref" href="StlcProp.html#t:35"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="Stlc.html#STLC.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="StlcProp.html#t:35"><span class="id" title="variable">t</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Corollary</span> <a id="STLCProp.soundness" class="idref" href="#STLCProp.soundness"><span class="id" title="lemma">soundness</span></a> : <span class="id" title="keyword">∀</span> <a id="t:36" class="idref" href="#t:36"><span class="id" title="binder">t</span></a> <a id="t':37" class="idref" href="#t':37"><span class="id" title="binder">t'</span></a> <a id="T:38" class="idref" href="#T:38"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:36"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:38"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="StlcProp.html#t:36"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="StlcProp.html#t':37"><span class="id" title="variable">t'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">~(</span></a><a class="idref" href="StlcProp.html#STLCProp.stuck"><span class="id" title="definition">stuck</span></a> <a class="idref" href="StlcProp.html#t':37"><span class="id" title="variable">t'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">)</span></a>.<br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">t'</span> <span class="id" title="var">T</span> <span class="id" title="var">Hhas_type</span> <span class="id" title="var">Hmulti</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="StlcProp.html#STLCProp.stuck"><span class="id" title="definition">stuck</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> [<span class="id" title="var">Hnf</span> <span class="id" title="var">Hnot_val</span>]. <span class="id" title="tactic">unfold</span> <a class="idref" href="Smallstep.html#normal_form"><span class="id" title="definition">normal_form</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">Hnf</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Hmulti</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
</div>
</div>

<div class="doc">
<font size=-2>&#9744;</font> 
</div>

<div class="doc">
<a id="lab245"></a><h1 class="section">Uniqueness of Types</h1>

<div class="paragraph"> </div>

<a id="lab246"></a><h4 class="section">Exercise: 3 stars, standard (unique_types)</h4>
 Another nice property of the STLC is that types are unique: a
    given term (in a given context) has at most one type. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="STLCProp.unique_types" class="idref" href="#STLCProp.unique_types"><span class="id" title="lemma">unique_types</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:39" class="idref" href="#Gamma:39"><span class="id" title="binder">Gamma</span></a> <a id="e:40" class="idref" href="#e:40"><span class="id" title="binder">e</span></a> <a id="T:41" class="idref" href="#T:41"><span class="id" title="binder">T</span></a> <a id="T':42" class="idref" href="#T':42"><span class="id" title="binder">T'</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#e:40"><span class="id" title="variable">e</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:41"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#e:40"><span class="id" title="variable">e</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T':42"><span class="id" title="variable">T'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="StlcProp.html#T:41"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="StlcProp.html#T':42"><span class="id" title="variable">T'</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab247"></a><h1 class="section">Context Invariance</h1>

<div class="paragraph"> </div>

 A standard technical lemma of a type system is
  <i>context invariance</i>. It states that typing is preserved
under "inessential changes" to the context <span class="inlinecode"><span class="id" title="var">Gamma</span></span> -- in
particular, changes that do not affect any of the free
variables of the term. Next, we establish this property
for our system.  
<div class="paragraph"> </div>

 First, we need to define the <i>free variables</i> in a term --
i.e., variables that are used in the term in positions
that are <i>not</i> in the scope of an enclosing function
abstraction binding a variable of the same name.

<div class="paragraph"> </div>

More technically, a variable <span class="inlinecode"><span class="id" title="var">x</span></span> <i>appears free in</i> a term <i>t</i>
if <span class="inlinecode"><span class="id" title="var">t</span></span> contains some occurrence of <span class="inlinecode"><span class="id" title="var">x</span></span> that is not under
an abstraction labeled <span class="inlinecode"><span class="id" title="var">x</span></span>. For example:
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">y</span></span> appears free, but <span class="inlinecode"><span class="id" title="var">x</span></span> does not, in <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>→<span class="id" title="var">U</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span>

</li>
<li> both <span class="inlinecode"><span class="id" title="var">x</span></span> and <span class="inlinecode"><span class="id" title="var">y</span></span> appear free in <span class="inlinecode">(\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>→<span class="id" title="var">U</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span>)</span> <span class="inlinecode"><span class="id" title="var">x</span></span>

</li>
<li> no variables appear free in <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>→<span class="id" title="var">U</span>,</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">T</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span>

</li>
</ul>

<div class="paragraph"> </div>

  Formally: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="STLCProp.appears_free_in" class="idref" href="#STLCProp.appears_free_in"><span class="id" title="inductive">appears_free_in</span></a> (<a id="x:43" class="idref" href="#x:43"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCProp.afi_var" class="idref" href="#STLCProp.afi_var"><span class="id" title="constructor">afi_var</span></a> : <a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCProp.afi_app1" class="idref" href="#STLCProp.afi_app1"><span class="id" title="constructor">afi_app1</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:46" class="idref" href="#t<sub>1</sub>:46"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:47" class="idref" href="#t<sub>2</sub>:47"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="StlcProp.html#t<sub>1</sub>:46"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="StlcProp.html#t<sub>1</sub>:46"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="StlcProp.html#t<sub>2</sub>:47"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCProp.afi_app2" class="idref" href="#STLCProp.afi_app2"><span class="id" title="constructor">afi_app2</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:48" class="idref" href="#t<sub>1</sub>:48"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:49" class="idref" href="#t<sub>2</sub>:49"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="StlcProp.html#t<sub>2</sub>:49"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="StlcProp.html#t<sub>1</sub>:48"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="StlcProp.html#t<sub>2</sub>:49"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCProp.afi_abs" class="idref" href="#STLCProp.afi_abs"><span class="id" title="constructor">afi_abs</span></a> : <span class="id" title="keyword">∀</span> <a id="y:50" class="idref" href="#y:50"><span class="id" title="binder">y</span></a> <a id="T<sub>1</sub>:51" class="idref" href="#T<sub>1</sub>:51"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="t<sub>1</sub>:52" class="idref" href="#t<sub>1</sub>:52"><span class="id" title="binder">t<sub>1</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#y:50"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'&lt;&gt;'_x"><span class="id" title="notation">≠</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="StlcProp.html#t<sub>1</sub>:52"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="StlcProp.html#y:50"><span class="id" title="variable">y</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="StlcProp.html#T<sub>1</sub>:51"><span class="id" title="variable">T<sub>1</sub></span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="StlcProp.html#t<sub>1</sub>:52"><span class="id" title="variable">t<sub>1</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCProp.afi_if<sub>1</sub>" class="idref" href="#STLCProp.afi_if<sub>1</sub>"><span class="id" title="constructor">afi_if<sub>1</sub></span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:53" class="idref" href="#t<sub>1</sub>:53"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:54" class="idref" href="#t<sub>2</sub>:54"><span class="id" title="binder">t<sub>2</sub></span></a> <a id="t<sub>3</sub>:55" class="idref" href="#t<sub>3</sub>:55"><span class="id" title="binder">t<sub>3</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="StlcProp.html#t<sub>1</sub>:53"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="StlcProp.html#t<sub>1</sub>:53"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="StlcProp.html#t<sub>2</sub>:54"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="StlcProp.html#t<sub>3</sub>:55"><span class="id" title="variable">t<sub>3</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCProp.afi_if<sub>2</sub>" class="idref" href="#STLCProp.afi_if<sub>2</sub>"><span class="id" title="constructor">afi_if<sub>2</sub></span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:56" class="idref" href="#t<sub>1</sub>:56"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:57" class="idref" href="#t<sub>2</sub>:57"><span class="id" title="binder">t<sub>2</sub></span></a> <a id="t<sub>3</sub>:58" class="idref" href="#t<sub>3</sub>:58"><span class="id" title="binder">t<sub>3</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="StlcProp.html#t<sub>2</sub>:57"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="StlcProp.html#t<sub>1</sub>:56"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="StlcProp.html#t<sub>2</sub>:57"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="StlcProp.html#t<sub>3</sub>:58"><span class="id" title="variable">t<sub>3</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCProp.afi_if<sub>3</sub>" class="idref" href="#STLCProp.afi_if<sub>3</sub>"><span class="id" title="constructor">afi_if<sub>3</sub></span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:59" class="idref" href="#t<sub>1</sub>:59"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:60" class="idref" href="#t<sub>2</sub>:60"><span class="id" title="binder">t<sub>2</sub></span></a> <a id="t<sub>3</sub>:61" class="idref" href="#t<sub>3</sub>:61"><span class="id" title="binder">t<sub>3</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="StlcProp.html#t<sub>3</sub>:61"><span class="id" title="variable">t<sub>3</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#appears_free_in:44"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="StlcProp.html#t<sub>1</sub>:59"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="StlcProp.html#t<sub>2</sub>:60"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="StlcProp.html#t<sub>3</sub>:61"><span class="id" title="variable">t<sub>3</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="StlcProp.html#appears_free_in"><span class="id" title="inductive">appears_free_in</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
The <i>free variables</i> of a term are just the variables that appear
    free in it.  A term with no free variables is said to be
    <i>closed</i>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="STLCProp.closed" class="idref" href="#STLCProp.closed"><span class="id" title="definition">closed</span></a> (<a id="t:62" class="idref" href="#t:62"><span class="id" title="binder">t</span></a>:<a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <a id="x:63" class="idref" href="#x:63"><span class="id" title="binder">x</span></a>, <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="StlcProp.html#STLCProp.appears_free_in"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:63"><span class="id" title="variable">x</span></a> <a class="idref" href="StlcProp.html#t:62"><span class="id" title="variable">t</span></a>.<br/>
</div>

<div class="doc">
An <i>open</i> term is one that may contain free variables.  (I.e., every
    term is an open term; the closed terms are a subset of the open ones.
    "Open" precisely means "possibly containing free variables.") 
<div class="paragraph"> </div>

<a id="lab248"></a><h4 class="section">Exercise: 1 star, standard (afi)</h4>
 In the space below, write out the rules of the <span class="inlinecode"><span class="id" title="var">appears_free_in</span></span>
    relation in informal inference-rule notation.  (Use whatever
    notational conventions you like -- the point of the exercise is
    just for you to think a bit about the meaning of each rule.)
    Although this is a rather low-level, technical definition,
    understanding it is crucial to understanding substitution and its
    properties, which are really the crux of the lambda-calculus. 
</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="STLCProp.manual_grade_for_afi" class="idref" href="#STLCProp.manual_grade_for_afi"><span class="id" title="definition">manual_grade_for_afi</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 Next, we show that if a variable <span class="inlinecode"><span class="id" title="var">x</span></span> appears free in a term <span class="inlinecode"><span class="id" title="var">t</span></span>,
    and if we know <span class="inlinecode"><span class="id" title="var">t</span></span> is well typed in context <span class="inlinecode"><span class="id" title="var">Gamma</span></span>, then it
    must be the case that <span class="inlinecode"><span class="id" title="var">Gamma</span></span> assigns a type to <span class="inlinecode"><span class="id" title="var">x</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCProp.free_in_context" class="idref" href="#STLCProp.free_in_context"><span class="id" title="lemma">free_in_context</span></a> : <span class="id" title="keyword">∀</span> <a id="x:64" class="idref" href="#x:64"><span class="id" title="binder">x</span></a> <a id="t:65" class="idref" href="#t:65"><span class="id" title="binder">t</span></a> <a id="T:66" class="idref" href="#T:66"><span class="id" title="binder">T</span></a> <a id="Gamma:67" class="idref" href="#Gamma:67"><span class="id" title="binder">Gamma</span></a>,<br/>
&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#STLCProp.appears_free_in"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:64"><span class="id" title="variable">x</span></a> <a class="idref" href="StlcProp.html#t:65"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma:67"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:65"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:66"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="T':68" class="idref" href="#T':68"><span class="id" title="binder">T'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="StlcProp.html#Gamma:67"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="StlcProp.html#x:64"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="StlcProp.html#T':68"><span class="id" title="variable">T'</span></a>.<br/>
</div>

<div class="doc">
<i>Proof</i>: We show, by induction on the proof that <span class="inlinecode"><span class="id" title="var">x</span></span> appears free
    in <span class="inlinecode"><span class="id" title="var">t</span></span>, that, for all contexts <span class="inlinecode"><span class="id" title="var">Gamma</span></span>, if <span class="inlinecode"><span class="id" title="var">t</span></span> is well typed under
    <span class="inlinecode"><span class="id" title="var">Gamma</span></span>, then <span class="inlinecode"><span class="id" title="var">Gamma</span></span> assigns some type to <span class="inlinecode"><span class="id" title="var">x</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last rule used is <span class="inlinecode"><span class="id" title="var">afi_var</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">x</span></span>, and from the
      assumption that <span class="inlinecode"><span class="id" title="var">t</span></span> is well typed under <span class="inlinecode"><span class="id" title="var">Gamma</span></span> we have
      immediately that <span class="inlinecode"><span class="id" title="var">Gamma</span></span> assigns a type to <span class="inlinecode"><span class="id" title="var">x</span></span>.

<div class="paragraph"> </div>


</li>
<li> If the last rule used is <span class="inlinecode"><span class="id" title="var">afi_app1</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" title="var">x</span></span>
      appears free in <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>.  Since <span class="inlinecode"><span class="id" title="var">t</span></span> is well typed under <span class="inlinecode"><span class="id" title="var">Gamma</span></span>, we
      can see from the typing rules that <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> must also be, and the IH
      then tells us that <span class="inlinecode"><span class="id" title="var">Gamma</span></span> assigns <span class="inlinecode"><span class="id" title="var">x</span></span> a type.

<div class="paragraph"> </div>


</li>
<li> Almost all the other cases are similar: <span class="inlinecode"><span class="id" title="var">x</span></span> appears free in a
      subterm of <span class="inlinecode"><span class="id" title="var">t</span></span>, and since <span class="inlinecode"><span class="id" title="var">t</span></span> is well typed under <span class="inlinecode"><span class="id" title="var">Gamma</span></span>, we
      know the subterm of <span class="inlinecode"><span class="id" title="var">t</span></span> in which <span class="inlinecode"><span class="id" title="var">x</span></span> appears is well typed under
      <span class="inlinecode"><span class="id" title="var">Gamma</span></span> as well, and the IH gives us exactly the conclusion we
      want.

<div class="paragraph"> </div>


</li>
<li> The only remaining case is <span class="inlinecode"><span class="id" title="var">afi_abs</span></span>.  In this case <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span>
      <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">T<sub>1</sub></span>,<span class="id" title="var">t<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" title="var">x</span></span> appears free in <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>, and we also know that
      <span class="inlinecode"><span class="id" title="var">x</span></span> is different from <span class="inlinecode"><span class="id" title="var">y</span></span>.  The difference from the previous
      cases is that, whereas <span class="inlinecode"><span class="id" title="var">t</span></span> is well typed under <span class="inlinecode"><span class="id" title="var">Gamma</span></span>, its body
      <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> is well typed under <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>1</sub></span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span>, so the IH allows us
      to conclude that <span class="inlinecode"><span class="id" title="var">x</span></span> is assigned some type by the extended
      context <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>1</sub></span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span>.  To conclude that <span class="inlinecode"><span class="id" title="var">Gamma</span></span> assigns a
      type to <span class="inlinecode"><span class="id" title="var">x</span></span>, we appeal to lemma <span class="inlinecode"><span class="id" title="var">update_neq</span></span>, noting that <span class="inlinecode"><span class="id" title="var">x</span></span>
      and <span class="inlinecode"><span class="id" title="var">y</span></span> are different variables. 
</li>
</ul>

<div class="paragraph"> </div>

<a id="lab249"></a><h4 class="section">Exercise: 2 stars, standard (free_in_context)</h4>
 Complete the following proof. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">H</span> <span class="id" title="var">H<sub>0</sub></span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">H</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span>; <span class="id" title="tactic">try</span> <span class="id" title="tactic">solve</span> [<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>; <span class="id" title="tactic">eauto</span>].<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 From the <span class="inlinecode"><span class="id" title="var">free_in_context</span></span> lemma, it immediately follows that any
    term <span class="inlinecode"><span class="id" title="var">t</span></span> that is well typed in the empty context is closed (it has
    no free variables). 
<div class="paragraph"> </div>

<a id="lab250"></a><h4 class="section">Exercise: 2 stars, standard, optional (typable_empty__closed)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Corollary</span> <a id="STLCProp.typable_empty__closed" class="idref" href="#STLCProp.typable_empty__closed"><span class="id" title="lemma">typable_empty__closed</span></a> : <span class="id" title="keyword">∀</span> <a id="t:69" class="idref" href="#t:69"><span class="id" title="binder">t</span></a> <a id="T:70" class="idref" href="#T:70"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:69"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:70"><span class="id" title="variable">T</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#STLCProp.closed"><span class="id" title="definition">closed</span></a> <a class="idref" href="StlcProp.html#t:69"><span class="id" title="variable">t</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 Next, we establish <i>context_invariance</i>.
    It is useful in cases when we have a proof of some typing relation
    <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>, and we need to replace <span class="inlinecode"><span class="id" title="var">Gamma</span></span> by a different
    context <span class="inlinecode"><span class="id" title="var">Gamma'</span></span>.  When is it safe to do this?  Intuitively, it
    must at least be the case that <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> assigns the same types as
    <span class="inlinecode"><span class="id" title="var">Gamma</span></span> to all the variables that appear free in <span class="inlinecode"><span class="id" title="var">t</span></span>. In fact,
    this is the only condition that is needed. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCProp.context_invariance" class="idref" href="#STLCProp.context_invariance"><span class="id" title="lemma">context_invariance</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:71" class="idref" href="#Gamma:71"><span class="id" title="binder">Gamma</span></a> <a id="Gamma':72" class="idref" href="#Gamma':72"><span class="id" title="binder">Gamma'</span></a> <a id="t:73" class="idref" href="#t:73"><span class="id" title="binder">t</span></a> <a id="T:74" class="idref" href="#T:74"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma:71"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:73"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:74"><span class="id" title="variable">T</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <a id="x:75" class="idref" href="#x:75"><span class="id" title="binder">x</span></a>, <a class="idref" href="StlcProp.html#STLCProp.appears_free_in"><span class="id" title="inductive">appears_free_in</span></a> <a class="idref" href="StlcProp.html#x:75"><span class="id" title="variable">x</span></a> <a class="idref" href="StlcProp.html#t:73"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#Gamma:71"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="StlcProp.html#x:75"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="StlcProp.html#Gamma':72"><span class="id" title="variable">Gamma'</span></a> <a class="idref" href="StlcProp.html#x:75"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="StlcProp.html#Gamma':72"><span class="id" title="variable">Gamma'</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="StlcProp.html#t:73"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="StlcProp.html#T:74"><span class="id" title="variable">T</span></a>.<br/>
</div>

<div class="doc">
<i>Proof</i>: By induction on the derivation of <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last rule in the derivation was <span class="inlinecode"><span class="id" title="var">T_Var</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">x</span></span> and
      <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">T</span></span>.  By assumption, <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">T</span></span> as well, and hence
      <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> by <span class="inlinecode"><span class="id" title="var">T_Var</span></span>.

<div class="paragraph"> </div>


</li>
<li> If the last rule was <span class="inlinecode"><span class="id" title="var">T_Abs</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">T<sub>2</sub></span>,</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>, with <span class="inlinecode"><span class="id" title="var">T</span></span> <span class="inlinecode">=</span>
      <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>.  The induction
      hypothesis states that for any context <span class="inlinecode"><span class="id" title="var">Gamma''</span></span>, if <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;</span>
      <span class="inlinecode"><span class="id" title="var">Gamma</span></span> and <span class="inlinecode"><span class="id" title="var">Gamma''</span></span> assign the same types to all the free
      variables in <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>, then <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> has type <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span> under <span class="inlinecode"><span class="id" title="var">Gamma''</span></span>.
      Let <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> be a context which agrees with <span class="inlinecode"><span class="id" title="var">Gamma</span></span> on the free
      variables in <span class="inlinecode"><span class="id" title="var">t</span></span>; we must show <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">T<sub>2</sub></span>,</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>.

<div class="paragraph"> </div>

      By <span class="inlinecode"><span class="id" title="var">T_Abs</span></span>, it suffices to show that <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span>
      <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span>.  By the IH (setting <span class="inlinecode"><span class="id" title="var">Gamma''</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;<span class="id" title="var">Gamma'</span></span>), it
      suffices to show that <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;<span class="id" title="var">Gamma</span></span> and <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;<span class="id" title="var">Gamma'</span></span> agree
      on all the variables that appear free in <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>.

<div class="paragraph"> </div>

      Any variable occurring free in <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> must be either <span class="inlinecode"><span class="id" title="var">y</span></span> or some
      other variable.  <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> and <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> clearly
      agree on <span class="inlinecode"><span class="id" title="var">y</span></span>.  Otherwise, note that any variable other than <span class="inlinecode"><span class="id" title="var">y</span></span>
      that occurs free in <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> also occurs free in <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">T<sub>2</sub></span>,</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>,
      and by assumption <span class="inlinecode"><span class="id" title="var">Gamma</span></span> and <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> agree on all such
      variables; hence so do <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> and <span class="inlinecode"><span class="id" title="var">y</span><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span><span class="id" title="var">T<sub>2</sub></span>;</span> <span class="inlinecode"><span class="id" title="var">Gamma'</span></span>.

<div class="paragraph"> </div>


</li>
<li> If the last rule was <span class="inlinecode"><span class="id" title="var">T_App</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>, with <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span>
      <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">T</span></span> and <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span>.  One induction
      hypothesis states that for all contexts <span class="inlinecode"><span class="id" title="var">Gamma'</span></span>, if <span class="inlinecode"><span class="id" title="var">Gamma'</span></span>
      agrees with <span class="inlinecode"><span class="id" title="var">Gamma</span></span> on the free variables in <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>, then <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> has
      type <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">T</span></span> under <span class="inlinecode"><span class="id" title="var">Gamma'</span></span>; there is a similar IH for <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>.
      We must show that <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> also has type <span class="inlinecode"><span class="id" title="var">T</span></span> under <span class="inlinecode"><span class="id" title="var">Gamma'</span></span>,
      given the assumption that <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> agrees with <span class="inlinecode"><span class="id" title="var">Gamma</span></span> on all
      the free variables in <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>.  By <span class="inlinecode"><span class="id" title="var">T_App</span></span>, it suffices to show
      that <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> each have the same type under <span class="inlinecode"><span class="id" title="var">Gamma'</span></span> as
      under <span class="inlinecode"><span class="id" title="var">Gamma</span></span>.  But all free variables in <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> are also free in
      <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>, and similarly for <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>; hence the desired result
      follows from the induction hypotheses. 
</li>
</ul>

<div class="paragraph"> </div>

<a id="lab251"></a><h4 class="section">Exercise: 3 stars, standard, optional (context_invariance)</h4>
 Complete the following proof. 
</div>
<div class="code">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma'</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">intros</span>; <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab252"></a><h1 class="section">Additional Exercises</h1>

<div class="paragraph"> </div>

<a id="lab253"></a><h4 class="section">Exercise: 1 star, standard (progress_preservation_statement)</h4>
 Without peeking at their statements above, write down the progress
    and preservation theorems for the simply typed lambda-calculus (as
    Coq theorems).
    You can write <span class="inlinecode"><span class="id" title="var">Admitted</span></span> for the proofs. 
</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="STLCProp.manual_grade_for_progress_preservation_statement" class="idref" href="#STLCProp.manual_grade_for_progress_preservation_statement"><span class="id" title="definition">manual_grade_for_progress_preservation_statement</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab254"></a><h4 class="section">Exercise: 2 stars, standard (stlc_variation1)</h4>
 Suppose we add a new term <span class="inlinecode"><span class="id" title="var">zap</span></span> with the following reduction rule
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Zap) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">t <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> zap</td>
  <td></td>
</td>
</table></center>and the following typing rule:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Zap) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; zap &#x2208; T</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain truee in
    the presence of these rules?  For each property, write either
    "remains true" or "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" title="var">step</span></span>

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Progress

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Preservation

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="STLCProp.manual_grade_for_stlc_variation1" class="idref" href="#STLCProp.manual_grade_for_stlc_variation1"><span class="id" title="definition">manual_grade_for_stlc_variation1</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab255"></a><h4 class="section">Exercise: 2 stars, standard (stlc_variation2)</h4>
 Suppose instead that we add a new term <span class="inlinecode"><span class="id" title="var">foo</span></span> with the following
    reduction rules:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Foo1) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(\x:A, x) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> foo</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Foo2) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">foo <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> true</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" title="var">step</span></span>

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Progress

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Preservation

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="STLCProp.manual_grade_for_stlc_variation2" class="idref" href="#STLCProp.manual_grade_for_stlc_variation2"><span class="id" title="definition">manual_grade_for_stlc_variation2</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab256"></a><h4 class="section">Exercise: 2 stars, standard (stlc_variation3)</h4>
 Suppose instead that we remove the rule <span class="inlinecode"><span class="id" title="var">ST_App1</span></span> from the <span class="inlinecode"><span class="id" title="var">step</span></span>
    relation. Which of the following properties of the STLC remain
    true in the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" title="var">step</span></span>

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Progress

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Preservation

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="STLCProp.manual_grade_for_stlc_variation3" class="idref" href="#STLCProp.manual_grade_for_stlc_variation3"><span class="id" title="definition">manual_grade_for_stlc_variation3</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab257"></a><h4 class="section">Exercise: 2 stars, standard, optional (stlc_variation4)</h4>
 Suppose instead that we add the following new rule to the
    reduction relation:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_FunnyIfTrue) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(if true then t<sub>1</sub> else t<sub>2</sub>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> true</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" title="var">step</span></span>

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Progress

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Preservation

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab258"></a><h4 class="section">Exercise: 2 stars, standard, optional (stlc_variation5)</h4>
 Suppose instead that we add the following new rule to the typing
    relation:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>1</sub> &#x2208; Bool<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Bool<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>Bool</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>2</sub> &#x2208; Bool</td>
  <td class="infrulenamecol" rowspan="3">
    (T_FunnyApp) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>1</sub> t<sub>2</sub> &#x2208; Bool</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" title="var">step</span></span>

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Progress

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Preservation

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab259"></a><h4 class="section">Exercise: 2 stars, standard, optional (stlc_variation6)</h4>
 Suppose instead that we add the following new rule to the typing
    relation:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>1</sub> &#x2208; Bool</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>2</sub> &#x2208; Bool</td>
  <td class="infrulenamecol" rowspan="3">
    (T_FunnyApp') &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>1</sub> t<sub>2</sub> &#x2208; Bool</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" title="var">step</span></span>

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Progress

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Preservation

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab260"></a><h4 class="section">Exercise: 2 stars, standard, optional (stlc_variation7)</h4>
 Suppose we add the following new rule to the typing relation
    of the STLC:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_FunnyAbs) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; \x:Bool,t &#x2208; Bool</td>
  <td></td>
</td>
</table></center>    Which of the following properties of the STLC remain true in
    the presence of this rule?  For each one, write either
    "remains true" or else "becomes false." If a property becomes
    false, give a counterexample.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" title="var">step</span></span>

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Progress

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<ul class="doclist">
<li> Preservation

</li>
</ul>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <font size=-2>&#9744;</font> 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="StlcProp.html#STLCProp"><span class="id" title="module">STLCProp</span></a>.<br/>
</div>

<div class="doc">
<a id="lab261"></a><h2 class="section">Exercise: STLC with Arithmetic</h2>

<div class="paragraph"> </div>

 To see how the STLC might function as the core of a real
    programming language, let's extend it with a concrete base
    type of numbers and some constants and primitive
    operators. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="STLCArith" class="idref" href="#STLCArith"><span class="id" title="module">STLCArith</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">STLC</span>.<br/>
</div>

<div class="doc">
To types, we add a base type of natural numbers (and remove
    booleans, for brevity). 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="STLCArith.ty" class="idref" href="#STLCArith.ty"><span class="id" title="inductive">ty</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCArith.Ty_Arrow" class="idref" href="#STLCArith.Ty_Arrow"><span class="id" title="constructor">Ty_Arrow</span></a> : <a class="idref" href="StlcProp.html#ty:76"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#ty:76"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#ty:76"><span class="id" title="inductive">ty</span></a><br/>
&nbsp;&nbsp;| <a id="STLCArith.Ty_Nat" class="idref" href="#STLCArith.Ty_Nat"><span class="id" title="constructor">Ty_Nat</span></a>  : <a class="idref" href="StlcProp.html#ty:76"><span class="id" title="inductive">ty</span></a>.<br/>
</div>

<div class="doc">
To terms, we add natural number constants, along with
    successor, predecessor, multiplication, and zero-testing. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="STLCArith.tm" class="idref" href="#STLCArith.tm"><span class="id" title="inductive">tm</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCArith.tm_var" class="idref" href="#STLCArith.tm_var"><span class="id" title="constructor">tm_var</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCArith.tm_app" class="idref" href="#STLCArith.tm_app"><span class="id" title="constructor">tm_app</span></a> : <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCArith.tm_abs" class="idref" href="#STLCArith.tm_abs"><span class="id" title="constructor">tm_abs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#STLCArith.ty"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCArith.tm_const" class="idref" href="#STLCArith.tm_const"><span class="id" title="constructor">tm_const</span></a>  : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCArith.tm_succ" class="idref" href="#STLCArith.tm_succ"><span class="id" title="constructor">tm_succ</span></a> : <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCArith.tm_pred" class="idref" href="#STLCArith.tm_pred"><span class="id" title="constructor">tm_pred</span></a> : <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCArith.tm_mult" class="idref" href="#STLCArith.tm_mult"><span class="id" title="constructor">tm_mult</span></a> : <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCArith.tm_if<sub>0</sub>" class="idref" href="#STLCArith.tm_if<sub>0</sub>"><span class="id" title="constructor">tm_if<sub>0</sub></span></a> : <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="StlcProp.html#tm:78"><span class="id" title="inductive">tm</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="b7a9b9a203ccd3bcc08d197b4bd66751" class="idref" href="#b7a9b9a203ccd3bcc08d197b4bd66751"><span class="id" title="notation">&quot;</span></a>{ x }" := <span class="id" title="var">x</span> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="e1de1169bc0019026b5cb83a8c525cf<sub>0</sub>" class="idref" href="#e1de1169bc0019026b5cb83a8c525cf<sub>0</sub>"><span class="id" title="notation">&quot;</span></a>&lt;{ e }&gt;" := <span class="id" title="var">e</span> (<span class="id" title="var">e</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="c64141a2c968875f76b153b3f89e4590" class="idref" href="#c64141a2c968875f76b153b3f89e4590"><span class="id" title="notation">&quot;</span></a>( x )" := <span class="id" title="var">x</span> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCArith.:stlc::x" class="idref" href="#STLCArith.:stlc::x"><span class="id" title="notation">&quot;</span></a>x" := <span class="id" title="var">x</span> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCArith.:stlc::x_'-&gt;'_x" class="idref" href="#STLCArith.:stlc::x_'-&gt;'_x"><span class="id" title="notation">&quot;</span></a>S <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> T" := (<a class="idref" href="StlcProp.html#STLCArith.Ty_Arrow"><span class="id" title="constructor">Ty_Arrow</span></a> <span class="id" title="var">S</span> <span class="id" title="var">T</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCArith.:stlc::x_x" class="idref" href="#STLCArith.:stlc::x_x"><span class="id" title="notation">&quot;</span></a>x y" := (<a class="idref" href="StlcProp.html#STLCArith.tm_app"><span class="id" title="constructor">tm_app</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="be974cae9d385d4b1716dcf71390f506" class="idref" href="#be974cae9d385d4b1716dcf71390f506"><span class="id" title="notation">&quot;</span></a>\ x : t , y" :=<br/>
&nbsp;&nbsp;(<a class="idref" href="StlcProp.html#STLCArith.tm_abs"><span class="id" title="constructor">tm_abs</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> <span class="id" title="var">y</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">t</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">y</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="StlcProp.html#STLCArith.tm_var"><span class="id" title="constructor">tm_var</span></a> <a class="idref" href="StlcProp.html#STLCArith.tm_var"><span class="id" title="constructor">:</span></a> <a class="idref" href="StlcProp.html#STLCArith.tm_var"><span class="id" title="constructor">string</span></a> <a class="idref" href="StlcProp.html#STLCArith.tm_var"><span class="id" title="constructor">&gt;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="StlcProp.html#STLCArith.tm_var"><span class="id" title="constructor">tm</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLCArith.:stlc::'Nat'" class="idref" href="#STLCArith.:stlc::'Nat'"><span class="id" title="notation">&quot;</span></a>'Nat'" := <a class="idref" href="StlcProp.html#STLCArith.Ty_Nat"><span class="id" title="constructor">Ty_Nat</span></a> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCArith.:stlc::'succ'_x" class="idref" href="#STLCArith.:stlc::'succ'_x"><span class="id" title="notation">&quot;</span></a>'succ' x" := (<a class="idref" href="StlcProp.html#STLCArith.tm_succ"><span class="id" title="constructor">tm_succ</span></a> <span class="id" title="var">x</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCArith.:stlc::'pred'_x" class="idref" href="#STLCArith.:stlc::'pred'_x"><span class="id" title="notation">&quot;</span></a>'pred' x" := (<a class="idref" href="StlcProp.html#STLCArith.tm_pred"><span class="id" title="constructor">tm_pred</span></a> <span class="id" title="var">x</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="9e884fda7db2a03161058fdfd11e2132" class="idref" href="#9e884fda7db2a03161058fdfd11e2132"><span class="id" title="notation">&quot;</span></a>x * y" := (<a class="idref" href="StlcProp.html#STLCArith.tm_mult"><span class="id" title="constructor">tm_mult</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCArith.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x" class="idref" href="#STLCArith.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">&quot;</span></a>'if<sub>0</sub>' x 'then' y 'else' z" :=<br/>
&nbsp;&nbsp;(<a class="idref" href="StlcProp.html#STLCArith.tm_if<sub>0</sub>"><span class="id" title="constructor">tm_if<sub>0</sub></span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 89,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">y</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">z</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="StlcProp.html#STLCArith.tm_const"><span class="id" title="constructor">tm_const</span></a> <a class="idref" href="StlcProp.html#STLCArith.tm_const"><span class="id" title="constructor">:</span></a> <a class="idref" href="StlcProp.html#STLCArith.tm_const"><span class="id" title="constructor">nat</span></a> <a class="idref" href="StlcProp.html#STLCArith.tm_const"><span class="id" title="constructor">&gt;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="StlcProp.html#STLCArith.tm_const"><span class="id" title="constructor">tm</span></a>.<br/>
</div>

<div class="doc">
<a id="lab262"></a><h4 class="section">Exercise: 5 stars, standard (stlc_arith)</h4>
 Finish formalizing the definition and properties of the STLC
    extended with arithmetic. This is a longer exercise. Specifically:

<div class="paragraph"> </div>

    1. Copy the core definitions for STLC that we went through,
        as well as the key lemmas and theorems, and paste them
        into the file at this point. Do not copy examples, exercises,
        etc. (In particular, make sure you don't copy any of the <font size=-2>&#9744;</font>
        comments at the end of exercises, to avoid confusing the
        autograder.)

<div class="paragraph"> </div>

        You should copy over five definitions:
<ul class="doclist">
<li> Fixpoint susbt

</li>
<li> Inductive value

</li>
<li> Inductive step

</li>
<li> Inductive has_type

</li>
<li> Inductive appears_free_in

</li>
</ul>

<div class="paragraph"> </div>

        And five theorems, with their proofs:
<ul class="doclist">
<li> Lemma weakening

</li>
<li> Lemma weakening_empty

</li>
<li> Lemma substitution_preserves_typing

</li>
<li> Theorem preservation

</li>
<li> Theorem progress

</li>
</ul>

<div class="paragraph"> </div>

        It will be helpful to also copy over "Reserved Notation",
        "Notation", and "Hint Constructors" for these things.

<div class="paragraph"> </div>

    2. Edit and extend the four definitions (subst, value, step,
        and has_type) so they are appropriate for the new STLC
        extended with arithmetic.

<div class="paragraph"> </div>

    3. Extend the proofs of all the five properties of the original
        STLC to deal with the new syntactic forms. Make sure Coq
        accepts the whole file. 
</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="STLCArith.manual_grade_for_stlc_arith" class="idref" href="#STLCArith.manual_grade_for_stlc_arith"><span class="id" title="definition">manual_grade_for_stlc_arith</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="StlcProp.html#STLCArith"><span class="id" title="module">STLCArith</span></a>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;2020-08-24&nbsp;16:13&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>